FDL - Nuprl Definition : es-seq

Nuprl Definition : es-seq

11,40

es-seq(es;S) ==

e1, e2:E. e1 before e2

(

(e2 < e1))

clarification:

es-seq(es;S)
==

e1:es-E(es), e2:es-E(es). e1 before e2

es-E(es)

(

es-causl(es; e2; e1))

Definitions x:A. B(x), P Q, x before y l, E, A, (e < e')

FDL editor aliases es-seq

Definitions	x:A. B(x), P Q, x before y l, E, A, (e < e')
FDL editor aliases	es-seq